<html>
<head><meta charset="utf-8"><title>coinduction unsoundness · wg-traits · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/index.html">wg-traits</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html">coinduction unsoundness</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="179476076"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179476076" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179476076">(Oct 30 2019 at 20:54)</a>:</h4>
<p>Well, in my quest to un-overengineer my fix, I managed to remove the recursion in <code>pursue_strand</code> (so no more <code>pursue_strand_recursively</code>)</p>



<a name="179476079"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179476079" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179476079">(Oct 30 2019 at 20:54)</a>:</h4>
<p>whoops?</p>



<a name="179479370"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179479370" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179479370">(Oct 30 2019 at 21:26)</a>:</h4>
<p>huh</p>



<a name="179479377"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179479377" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179479377">(Oct 30 2019 at 21:26)</a>:</h4>
<p>I don't really understand that :)</p>



<a name="179484995"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179484995" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179484995">(Oct 30 2019 at 22:42)</a>:</h4>
<p>(also, that "whoops?" was definitely sarcasm. Removing the recursion is great, I think)</p>



<a name="179485010"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179485010" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179485010">(Oct 30 2019 at 22:42)</a>:</h4>
<p>I'm cleaning up some last bits of things and then I'll make a PR :)</p>



<a name="179486705"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179486705" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179486705">(Oct 30 2019 at 23:10)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> <a href="https://github.com/rust-lang/chalk/pull/272" target="_blank" title="https://github.com/rust-lang/chalk/pull/272">https://github.com/rust-lang/chalk/pull/272</a></p>



<a name="179559260"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179559260" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179559260">(Oct 31 2019 at 18:08)</a>:</h4>
<blockquote>
<p>(also, that "whoops?" was definitely sarcasm. Removing the recursion is great, I think)</p>
</blockquote>
<p>interesting. I'll take a look later!</p>



<a name="179638900"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179638900" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179638900">(Nov 01 2019 at 16:06)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> Was wondering if you have had time to peek at the PR? I'm actually curious if it will solve the infinite stack growth problem in rust-analyzer since it removes the recursion. If nothing else, it might help make it easier to debug?</p>



<a name="179638923"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179638923" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179638923">(Nov 01 2019 at 16:06)</a>:</h4>
<p>I'm actually skimming it now</p>



<a name="179638957"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179638957" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179638957">(Nov 01 2019 at 16:07)</a>:</h4>
<p>Awesome</p>



<a name="179639180"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179639180" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179639180">(Nov 01 2019 at 16:10)</a>:</h4>
<p>basically, you made us loop in <code>pursue_strand</code>, instead of having it recursively invoke itself?</p>



<a name="179639251"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179639251" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179639251">(Nov 01 2019 at 16:10)</a>:</h4>
<p>I don't think this will help with that particular problem</p>



<a name="179639510"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179639510" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179639510">(Nov 01 2019 at 16:13)</a>:</h4>
<p>Yep, basically</p>



<a name="179639690"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179639690" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179639690">(Nov 01 2019 at 16:14)</a>:</h4>
<p>it may actually make it harder to debug :) --</p>



<a name="179639706"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179639706" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179639706">(Nov 01 2019 at 16:14)</a>:</h4>
<p>the problem there is that we are generating too many subgoals</p>



<a name="179639718"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179639718" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179639718">(Nov 01 2019 at 16:15)</a>:</h4>
<p>(maybe I'll try to look at that a bit more later on...)</p>



<a name="179639749"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179639749" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179639749">(Nov 01 2019 at 16:15)</a>:</h4>
<p>the stack growth part is just a side-effect from that</p>



<a name="179639779"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179639779" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179639779">(Nov 01 2019 at 16:15)</a>:</h4>
<p>Ah</p>



<a name="179639795"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179639795" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179639795">(Nov 01 2019 at 16:15)</a>:</h4>
<p>I briefly skimmed over that conversation, but didn't look closely</p>



<a name="179639910"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179639910" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179639910">(Nov 01 2019 at 16:17)</a>:</h4>
<p>Importantly, I don't think we lose any debug information with my changes though. Since I call the <code>pursue_strand</code> info_heading for each loop (whereas before it was each recursion)</p>



<a name="179640050"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179640050" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179640050">(Nov 01 2019 at 16:18)</a>:</h4>
<blockquote>
<p>basically, you made us loop in <code>pursue_strand</code>, instead of having it recursively invoke itself?</p>
</blockquote>
<p>good idea though :)</p>



<a name="179640099"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179640099" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179640099">(Nov 01 2019 at 16:19)</a>:</h4>
<p>Yeah, like I said, it sort of just fell out of the refactoring that I did to make what I was doing simpler</p>



<a name="179640133"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179640133" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179640133">(Nov 01 2019 at 16:19)</a>:</h4>
<p>On a related note, I've been wanting to rework the logic that collects cyclic strands into a local vector</p>



<a name="179640150"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179640150" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179640150">(Nov 01 2019 at 16:19)</a>:</h4>
<p>so that they are collected instead in the table and we can return back a "QuantumExceeded"</p>



<a name="179640213"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179640213" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179640213">(Nov 01 2019 at 16:20)</a>:</h4>
<p>this basically gives the caller more of a chance to interrupt and say "you know what, I don't care that much"</p>



<a name="179640221"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179640221" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179640221">(Nov 01 2019 at 16:20)</a>:</h4>
<p>(i.e., it lets them implement "fuel")</p>



<a name="179640337"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179640337" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179640337">(Nov 01 2019 at 16:21)</a>:</h4>
<p>Yeah, I did a little bit of tinkering with that at the start, but it ended up being mostly unnecessary for this change</p>



<a name="179640361"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179640361" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179640361">(Nov 01 2019 at 16:22)</a>:</h4>
<p>but definitely worth rethinking</p>



<a name="179894495"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179894495" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179894495">(Nov 05 2019 at 01:33)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> Okay, I've updated the PR for your comments</p>



<a name="179894550"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179894550" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179894550">(Nov 05 2019 at 01:34)</a>:</h4>
<p>I also went through and verified that no subgoals can be added when <code>allow_coinductive</code> is true</p>



<a name="179894638"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179894638" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179894638">(Nov 05 2019 at 01:36)</a>:</h4>
<p>See my github comment, but basically they are really only added in <code>push_initial_strands_instantiated</code>, which I would sort of expect</p>



<a name="179894728"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/179894728" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#179894728">(Nov 05 2019 at 01:38)</a>:</h4>
<p>Also, I've done some more cleanup/refactoring in my branch that removes <code>CanonicalStrand</code>s. Some of it touches this code, but I'll either just make a separate PR for those or just lump it in with the remove <code>CanonicalStrand</code> PR</p>



<a name="180068456"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180068456" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180068456">(Nov 06 2019 at 19:31)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> For your second suspicion, is that only in the context of coinduction or a more general problem?</p>



<a name="180218617"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180218617" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180218617">(Nov 08 2019 at 10:41)</a>:</h4>
<p><span class="user-mention" data-user-id="232957">@Jack Huey</span> I apologize for radio silence, I'm not sure what's been going on last few weeks but I've been very short of time. I'm skimming your branch now. I am starting to wonder if it'd be a good idea to factor out some of the cleanup work and land it separately, just to help concentrate the diff</p>



<a name="180218694"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180218694" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180218694">(Nov 08 2019 at 10:42)</a>:</h4>
<p>The code which propagates the <code>CanonicalStrand</code> out of <code>ensure_answer</code> feels... I'm not sure. Similar-ish to what I initially had in mind, but somehow more complicated.</p>
<p>Actually maybe it's a good idea for me to try to be more precise about what I had in mind, so I can compare it to what you have done. I've been doing this in my head but I've not written it down in detail.</p>



<a name="180218725"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180218725" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180218725">(Nov 08 2019 at 10:43)</a>:</h4>
<p>In short, what I had in mind was:</p>



<a name="180218732"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180218732" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180218732">(Nov 08 2019 at 10:43)</a>:</h4>
<p>When a cycle occurs, we would take the goal and add it to a list in the <code>Strand</code>, let's call it <code>delayed_coinductive_subgoals</code> -- this is basically what you did to start.</p>



<a name="180218791"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180218791" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180218791">(Nov 08 2019 at 10:44)</a>:</h4>
<p>But then, when the other subgoals have (successfully) completed, I was <em>imagining</em> we would produce an answer, but that answer would include the delayed subgoals as well (effectively like the old delayed literals)</p>



<a name="180218808"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180218808" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180218808">(Nov 08 2019 at 10:45)</a>:</h4>
<p>But when you incorporate the answer from another table, if it was delayed on yourself, you would remove that goal</p>



<a name="180218819"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180218819" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180218819">(Nov 08 2019 at 10:45)</a>:</h4>
<p>There would ultimately have to be a loop much like the one you've added</p>



<a name="180218824"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180218824" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180218824">(Nov 08 2019 at 10:45)</a>:</h4>
<p>i.e., <code>ensure_root_answer</code>, if it gets back an answer with a delayed goal, would have to do a search</p>



<a name="180218826"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180218826" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180218826">(Nov 08 2019 at 10:45)</a>:</h4>
<p>so maybe this code is kind of equivalent</p>



<a name="180238359"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180238359" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180238359">(Nov 08 2019 at 15:14)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> No problem.</p>



<a name="180238381"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180238381" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180238381">(Nov 08 2019 at 15:14)</a>:</h4>
<p>So, with your approach</p>



<a name="180238428"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180238428" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180238428">(Nov 08 2019 at 15:15)</a>:</h4>
<p>the difference is mostly in where we "store" the "delayed subgoal"</p>



<a name="180238440"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180238440" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180238440">(Nov 08 2019 at 15:15)</a>:</h4>
<p>I think</p>



<a name="180238643"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180238643" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180238643">(Nov 08 2019 at 15:17)</a>:</h4>
<p><span class="user-mention" data-user-id="232957">@Jack Huey</span> this morning while making breakfast I think I saw how to describe my proposal</p>



<a name="180238654"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180238654" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180238654">(Nov 08 2019 at 15:17)</a>:</h4>
<p>but didn't haev time to write it down yet</p>



<a name="180238662"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180238662" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180238662">(Nov 08 2019 at 15:17)</a>:</h4>
<p>I will try to do that after compiler meeting</p>



<a name="180238669"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180238669" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180238669">(Nov 08 2019 at 15:17)</a>:</h4>
<p>But I was thinking, are youa ble to attend trait design meeting on Monday?</p>



<a name="180238670"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180238670" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180238670">(Nov 08 2019 at 15:17)</a>:</h4>
<p>No problem</p>



<a name="180238675"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180238675" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180238675">(Nov 08 2019 at 15:17)</a>:</h4>
<p>Maybe we should make this the topic?</p>



<a name="180238698"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180238698" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180238698">(Nov 08 2019 at 15:18)</a>:</h4>
<p>(Which wouldn't preclude you messing about with it, just seems like a good thing to discuss more broadly)</p>



<a name="180238752"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180238752" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180238752">(Nov 08 2019 at 15:18)</a>:</h4>
<p>I'd like to use those meetings to focus on work people are <em>doing</em> as much as possible, to help spread understanding</p>



<a name="180238757"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180238757" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180238757">(Nov 08 2019 at 15:18)</a>:</h4>
<p>Sure, I'll be around</p>



<a name="180238794"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180238794" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180238794">(Nov 08 2019 at 15:18)</a>:</h4>
<p>I'll also split out the refactoring-type stuff into a separate PR. That doesn't change anything</p>



<a name="180238818"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180238818" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180238818">(Nov 08 2019 at 15:18)</a>:</h4>
<p>that would be great</p>



<a name="180238866"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180238866" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180238866">(Nov 08 2019 at 15:19)</a>:</h4>
<p>As you can see, I also have the changes to remove <code>CanonicalStrand</code> ready</p>



<a name="180238886"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180238886" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180238886">(Nov 08 2019 at 15:19)</a>:</h4>
<p>(and have been working on the "fuel friendly" issue)</p>



<a name="180238986"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180238986" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180238986">(Nov 08 2019 at 15:20)</a>:</h4>
<p>the short version of what I had in mind is:</p>
<ul>
<li>
<p>extend <code>Answer</code> with "deferred subclauses" -- when you get a coinductive cycle, you push it in there<br>
    * unless the cycle is to yourself -- then you can just discard it</p>
</li>
<li>
<p>when incorporating an answer, we inline the deferred subclauses into our own list</p>
</li>
<li>by the time we reach root, all should be cleared<br>
    * but if you then query a subtable, and the answer has deferred subclauses, we need to "resume" that work, but it should be quick, and we can overwrite the answer in place</li>
</ul>
<p>ok, have to go back to other meeting ;)</p>



<a name="180238992"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180238992" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180238992">(Nov 08 2019 at 15:20)</a>:</h4>
<p>maybe that makes sense to you</p>



<a name="180239058"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180239058" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180239058">(Nov 08 2019 at 15:20)</a>:</h4>
<p>Yes, that was mostly the sense I was getting, so that makes sense</p>



<a name="180239063"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180239063" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180239063">(Nov 08 2019 at 15:20)</a>:</h4>
<p>I'll try it</p>



<a name="180242519"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180242519" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180242519">(Nov 08 2019 at 15:54)</a>:</h4>
<blockquote>
<div class="codehilite"><pre><span></span>* but if you then query a subtable, and the answer has deferred subclauses, we need to &quot;resume&quot; that work, but it should be quick, and we can overwrite the answer in place
</pre></div>


</blockquote>
<p>a few more notes on this:</p>
<p>I was thinking we could extend <code>pursue_strand</code> so that it takes the index where the index where the answer should be stored. Normally this would be one past the end (i.e., make a new answer). but if we are in <code>ensure_root_answer</code> and we get back answer with deferred subclauses, then we would create a new strand just solving those clauses and tell it to re-execute and overwrite the answer in place. </p>
<p>It is possible that this strand will fail -- in that case, we need to have a way to indicate that an answer was invalidated, and now represents just a failed path.</p>
<p>If you were to later invoke <code>ensure_answer</code> on a failed path, you get back some result that says "failed, but try the next answer".</p>



<a name="180245054"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180245054" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180245054">(Nov 08 2019 at 16:18)</a>:</h4>
<p>Err. You lost me.</p>



<a name="180245063"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180245063" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180245063">(Nov 08 2019 at 16:18)</a>:</h4>
<p>I'll have to think about that</p>



<a name="180245959"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180245959" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180245959">(Nov 08 2019 at 16:28)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> <a href="https://github.com/rust-lang/chalk/pull/279" target="_blank" title="https://github.com/rust-lang/chalk/pull/279">https://github.com/rust-lang/chalk/pull/279</a></p>



<a name="180245972"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180245972" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180245972">(Nov 08 2019 at 16:28)</a>:</h4>
<p>A PR with only recursion refactor changes</p>



<a name="180246197"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180246197" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180246197">(Nov 08 2019 at 16:30)</a>:</h4>
<p><span class="user-mention" data-user-id="232957">@Jack Huey</span> I started a <a href="https://hackmd.io/OJRi5OM6Twunw8ZmuLxfRA" target="_blank" title="https://hackmd.io/OJRi5OM6Twunw8ZmuLxfRA">hackmd document</a> summarizing what's going on, as a draft for meeting</p>



<a name="180246241"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180246241" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180246241">(Nov 08 2019 at 16:31)</a>:</h4>
<blockquote>
<p><span class="user-mention silent" data-user-id="116009">nikomatsakis</span> For your second suspicion, is that only in the context of coinduction or a more general problem?</p>
</blockquote>
<p>I also added an example illustrating the case I was suspicious about</p>



<a name="180246256"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180246256" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180246256">(Nov 08 2019 at 16:31)</a>:</h4>
<p>it is only a problem for coinduction, not a more general problem, the rest of the code should handle it just fine</p>



<a name="180246591"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180246591" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180246591">(Nov 08 2019 at 16:34)</a>:</h4>
<p>Ok I'll take a look</p>



<a name="180247247"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180247247" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180247247">(Nov 08 2019 at 16:40)</a>:</h4>
<blockquote>
<p>Err. You lost me.</p>
</blockquote>
<p>that last part is kind of an optimization, not that imp't</p>



<a name="180248545"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180248545" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180248545">(Nov 08 2019 at 16:52)</a>:</h4>
<p>let more notes in the hackmd, gotta run</p>



<a name="180248551"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180248551" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180248551">(Nov 08 2019 at 16:52)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> Looking at the unification example you gave, I don't think my branch would handle that</p>



<a name="180249739"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180249739" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180249739">(Nov 08 2019 at 17:03)</a>:</h4>
<p>Actually, I wrote a test for it. And (assuming my test is correct), it passes</p>



<a name="180255270"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180255270" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180255270">(Nov 08 2019 at 18:04)</a>:</h4>
<p>Ok, changing my test a bit reveals that while branch doesn't necessarily give a <em>wrong</em> answer, it does <code>Flounder</code> when it could give <code>NoSolutions</code></p>



<a name="180275018"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180275018" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180275018">(Nov 08 2019 at 21:39)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> Should I just got ahead and add back Stacker, but just wrap the <code>pursue_next_strand</code> call in <code>ensure_answer_recursively</code>?</p>



<a name="180275091"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180275091" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180275091">(Nov 08 2019 at 21:40)</a>:</h4>
<p>seems good -- or wrap calls to <code>ensure_answer_recursively</code></p>



<a name="180275096"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180275096" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180275096">(Nov 08 2019 at 21:40)</a>:</h4>
<p>but yeah basically when we enter into ensure-answer</p>



<a name="180275124"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180275124" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180275124">(Nov 08 2019 at 21:40)</a>:</h4>
<p>well, we only  want to wrap one spot</p>



<a name="180275140"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180275140" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180275140">(Nov 08 2019 at 21:40)</a>:</h4>
<p>I think your first suggestion was correct</p>



<a name="180275277"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180275277" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180275277">(Nov 08 2019 at 21:42)</a>:</h4>
<p>Ok I'll do that</p>



<a name="180275457"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180275457" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180275457">(Nov 08 2019 at 21:44)</a>:</h4>
<p>Also, the <code>remove CanonicalStrand</code> PR <em>should</em> be fairly straightforward too, I think</p>



<a name="180275556"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180275556" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180275556">(Nov 08 2019 at 21:45)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> PR is updated</p>



<a name="180312411"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180312411" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180312411">(Nov 09 2019 at 13:06)</a>:</h4>
<p><span class="user-mention" data-user-id="232957">@Jack Huey</span> ok, I've convinced myself that my coinduction scheme seems good -- but I've got to dig a bit more into the PR now with that revised understanding still</p>



<a name="180313189"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180313189" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180313189">(Nov 09 2019 at 13:27)</a>:</h4>
<p>Sure! The PR definitely doesn't handle the cases you brought up correctly</p>



<a name="180313235"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180313235" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180313235">(Nov 09 2019 at 13:28)</a>:</h4>
<p>I added tests for them</p>



<a name="180446945"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180446945" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180446945">(Nov 11 2019 at 18:22)</a>:</h4>
<p>I've maybe like 70% implemented your coinductive approach</p>



<a name="180447415"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180447415" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180447415">(Nov 11 2019 at 18:29)</a>:</h4>
<p>The only test not passing (including the new tests covering some of the new cases + removing the fixme on the existing test) is <code>test::wf_lowering::cyclic_wf_requirements</code></p>



<a name="180447464"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180447464" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180447464">(Nov 11 2019 at 18:29)</a>:</h4>
<p>But I need to add your variant 2 and 3 as tests</p>



<a name="180447472"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180447472" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180447472">(Nov 11 2019 at 18:29)</a>:</h4>
<p>I think those will fail</p>



<a name="180456985"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180456985" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180456985">(Nov 11 2019 at 20:25)</a>:</h4>
<p>Oops I was adding delayed_subgoals when incoporating an answer into <code>delayed_subgoals</code> instead of <code>subgoals</code></p>



<a name="180456989"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180456989" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180456989">(Nov 11 2019 at 20:25)</a>:</h4>
<p>Which exposes a different problem :)</p>



<a name="180458716"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180458716" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180458716">(Nov 11 2019 at 20:49)</a>:</h4>
<p>yeah that's not right :)</p>



<a name="180461489"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180461489" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180461489">(Nov 11 2019 at 21:27)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> ok, I'm maybe a bit stuck and have a question</p>



<a name="180461510"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180461510" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180461510">(Nov 11 2019 at 21:27)</a>:</h4>
<p>Still stuck on the same cyclic_wf_requirements test</p>



<a name="180461569"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180461569" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180461569">(Nov 11 2019 at 21:28)</a>:</h4>
<p>what's up</p>



<a name="180461702"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180461702" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180461702">(Nov 11 2019 at 21:28)</a>:</h4>
<p>One of the tables is returning an answer with a delayed subgoal of <code>InEnvironment { environment: Env([FromEnv(Unit)]), goal: WellFormed(&lt;?0 as Foo&gt;::Value: Foo) }</code></p>



<a name="180461746"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180461746" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180461746">(Nov 11 2019 at 21:29)</a>:</h4>
<p>Now, I feel like I need to do some sort of canonicalization somewhere that I'm not doing</p>



<a name="180461866"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180461866" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180461866">(Nov 11 2019 at 21:30)</a>:</h4>
<p>And that is getting pushed as a subgoal for the next strand up</p>



<a name="180461883"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180461883" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180461883">(Nov 11 2019 at 21:31)</a>:</h4>
<p>but then truncating that goal panics</p>



<a name="180461907"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180461907" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180461907">(Nov 11 2019 at 21:31)</a>:</h4>
<p>this may be because <code>?0</code> is an inference variable that got unified with <code>Unit</code></p>



<a name="180461911"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180461911" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180461911">(Nov 11 2019 at 21:31)</a>:</h4>
<p>depending on where you are printing the value</p>



<a name="180461915"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180461915" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180461915">(Nov 11 2019 at 21:31)</a>:</h4>
<p>it may not reflect all the unifications that happened</p>



<a name="180461964"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180461964" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180461964">(Nov 11 2019 at 21:32)</a>:</h4>
<p>I guess if you have a branch (or a "Draft" PR) that might be helpful</p>



<a name="180461979"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180461979" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180461979">(Nov 11 2019 at 21:32)</a>:</h4>
<p>oh wait no. it's <code>normalize_deep</code> that's panicing</p>



<a name="180462003"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180462003" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180462003">(Nov 11 2019 at 21:33)</a>:</h4>
<p>Sure I'll just push my changes to the same PR?</p>



<a name="180462110"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180462110" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180462110">(Nov 11 2019 at 21:34)</a>:</h4>
<p>which PR?</p>



<a name="180462111"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180462111" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180462111">(Nov 11 2019 at 21:34)</a>:</h4>
<p>seems ok</p>



<a name="180462136"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180462136" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180462136">(Nov 11 2019 at 21:35)</a>:</h4>
<p>The coinduction PR</p>



<a name="180462145"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180462145" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180462145">(Nov 11 2019 at 21:35)</a>:</h4>
<p>since I don't think we're going with the implementation I had</p>



<a name="180462153"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180462153" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180462153">(Nov 11 2019 at 21:35)</a>:</h4>
<p>though I'll keep it as a branch</p>



<a name="180462252"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180462252" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180462252">(Nov 11 2019 at 21:36)</a>:</h4>
<p>Ok <a href="https://github.com/rust-lang/chalk/pull/272" target="_blank" title="https://github.com/rust-lang/chalk/pull/272">https://github.com/rust-lang/chalk/pull/272</a> has the changes</p>



<a name="180463557"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180463557" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180463557">(Nov 11 2019 at 21:55)</a>:</h4>
<p>Oh shoot I got it to work</p>



<a name="180463606"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180463606" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180463606">(Nov 11 2019 at 21:56)</a>:</h4>
<p>I don't know if it's necessarily the right thing (probably isn't)</p>



<a name="180463625"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180463625" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180463625">(Nov 11 2019 at 21:56)</a>:</h4>
<p>and a couple tests fail so</p>



<a name="180463656"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180463656" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180463656">(Nov 11 2019 at 21:57)</a>:</h4>
<p>but I ended up canonicalizing the goal before storing it in the delayed_subgoals</p>



<a name="180465114"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180465114" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180465114">(Nov 11 2019 at 22:18)</a>:</h4>
<p>Oh</p>



<a name="180465116"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180465116" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180465116">(Nov 11 2019 at 22:18)</a>:</h4>
<p>So</p>



<a name="180465136"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180465136" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180465136">(Nov 11 2019 at 22:18)</a>:</h4>
<div class="codehilite"><pre><span></span>[chalk-engine/src/logic.rs:1046] &amp;delayed_subgoal = UCanonical {
    canonical: Canonical {
        value: InEnvironment {
            environment: Env([FromEnv(Unit)]),
            goal: WellFormed(&lt;Unit as Foo&gt;::Value: Foo),
        },
        binders: [],
    },
    universes: 1,
}
[chalk-engine/src/logic.rs:1047] &amp;table_goal = UCanonical {
    canonical: Canonical {
        value: InEnvironment {
            environment: Env([FromEnv(Unit)]),
            goal: WellFormed(Unit: Foo),
        },
        binders: [],
    },
    universes: 1,
}
</pre></div>



<a name="180465155"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180465155" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180465155">(Nov 11 2019 at 22:19)</a>:</h4>
<p>Those are the same</p>



<a name="180465192"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180465192" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180465192">(Nov 11 2019 at 22:19)</a>:</h4>
<p>So my "trivial self-cycle" check is not taking into account normalization</p>



<a name="180467434"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180467434" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180467434">(Nov 11 2019 at 22:58)</a>:</h4>
<p>Ok <span class="user-mention" data-user-id="116009">@nikomatsakis</span> I left some comments on the PR with some questions/comments</p>



<a name="180469326"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180469326" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180469326">(Nov 11 2019 at 23:39)</a>:</h4>
<p>ok <span class="user-mention" data-user-id="232957">@Jack Huey</span> will try to look soon!</p>



<a name="180482014"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180482014" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180482014">(Nov 12 2019 at 04:55)</a>:</h4>
<p>Ok a few thoughts:</p>



<a name="180482068"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180482068" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180482068">(Nov 12 2019 at 04:56)</a>:</h4>
<p>1) Are auto traits supposed to be non-enumerable or not? If so, how does this play into everything?</p>



<a name="180482148"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180482148" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180482148">(Nov 12 2019 at 04:59)</a>:</h4>
<p>(From what I can tell, removing the check for auto traits in <code>program_clauses</code> and the panic in <code>program_clauses_that_could_match</code> causes a few tests to return <code>[]</code> instead of <code>Flounder</code> irt. auto traits, but otherwise is fine.)</p>



<a name="180482182"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180482182" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180482182">(Nov 12 2019 at 05:00)</a>:</h4>
<p>(When making these changes <code>coinductive_conflicting2</code> test passes)</p>



<a name="180482299"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180482299" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180482299">(Nov 12 2019 at 05:01)</a>:</h4>
<p>2) My <code>coinductive_conflicting3</code> test still fails with the above changes, but because it finds a unique solution with <code>T=B</code>. The <code>T=A</code> subst isn't getting added to the <code>T: C1</code> table</p>



<a name="180522870"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180522870" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180522870">(Nov 12 2019 at 14:44)</a>:</h4>
<blockquote>
<p>1) Are auto traits supposed to be non-enumerable or not? If so, how does this play into everything?</p>
</blockquote>
<p>Are, yeah, a good question. I think that yes, auto traits are non-enumerable, more so than any other trait really. Probably we want to say that all traits are non-enumerable</p>



<a name="180556043"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180556043" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180556043">(Nov 12 2019 at 20:11)</a>:</h4>
<blockquote>
<p>Probably we want to say that all traits are non-enumerable</p>
</blockquote>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> that's a bold statement</p>



<a name="180556073"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180556073" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180556073">(Nov 12 2019 at 20:11)</a>:</h4>
<p>How does that effect things?</p>



<a name="180556101"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180556101" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180556101">(Nov 12 2019 at 20:11)</a>:</h4>
<p>that's what rustc does, at least</p>



<a name="180556123"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180556123" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180556123">(Nov 12 2019 at 20:11)</a>:</h4>
<p>it doesn't really matter to the engine at all?</p>



<a name="180556185"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180556185" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180556185">(Nov 12 2019 at 20:12)</a>:</h4>
<p>Well, it does sort of</p>



<a name="180556199"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180556199" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180556199">(Nov 12 2019 at 20:12)</a>:</h4>
<p>Why do you think so?</p>



<a name="180556213"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180556213" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180556213">(Nov 12 2019 at 20:12)</a>:</h4>
<p>Because it affects some tests?</p>



<a name="180556218"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180556218" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180556218">(Nov 12 2019 at 20:12)</a>:</h4>
<p>Or is there some other reason</p>



<a name="180556243"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180556243" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180556243">(Nov 12 2019 at 20:12)</a>:</h4>
<p>Actually, I guess the part that cares here isn't actually in chalk-engine</p>



<a name="180556293"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180556293" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180556293">(Nov 12 2019 at 20:13)</a>:</h4>
<p>But</p>



<a name="180556383"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180556383" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180556383">(Nov 12 2019 at 20:14)</a>:</h4>
<p>chalk-solve is Floundering a table in <code>program_clauses</code>for non-enumerable types</p>



<a name="180556399"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180556399" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180556399">(Nov 12 2019 at 20:14)</a>:</h4>
<p>seems ok</p>



<a name="180556406"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180556406" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180556406">(Nov 12 2019 at 20:14)</a>:</h4>
<p>so even though we can prove that something isn't possible, it flounders</p>



<a name="180556419"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180556419" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180556419">(Nov 12 2019 at 20:14)</a>:</h4>
<p>(also for auto traits)</p>



<a name="180556421"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180556421" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180556421">(Nov 12 2019 at 20:14)</a>:</h4>
<p>how can we prove it's not possible?</p>



<a name="180556437"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180556437" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180556437">(Nov 12 2019 at 20:15)</a>:</h4>
<p>So, this was one of your examples</p>



<a name="180556442"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180556442" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180556442">(Nov 12 2019 at 20:15)</a>:</h4>
<p>one sec</p>



<a name="180556475"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180556475" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180556475">(Nov 12 2019 at 20:15)</a>:</h4>
<div class="codehilite"><pre><span></span>C1(X) :- C2(Y), X = 22.
C2(X) :- C3(X), X = 44.
C3(X) :- C1(X), C2(X).
</pre></div>



<a name="180556487"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180556487" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180556487">(Nov 12 2019 at 20:15)</a>:</h4>
<p>I see</p>



<a name="180556500"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180556500" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180556500">(Nov 12 2019 at 20:15)</a>:</h4>
<p>Yeah, we may not be able to exercise that code path</p>



<a name="180556547"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180556547" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180556547">(Nov 12 2019 at 20:16)</a>:</h4>
<p>Without some "opt-in" to enumerating rules</p>



<a name="180556563"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180556563" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180556563">(Nov 12 2019 at 20:16)</a>:</h4>
<p>The test is here: <a href="https://github.com/rust-lang/chalk/pull/272/files#diff-721709466568566f24fc2e8634c40dcbR140" target="_blank" title="https://github.com/rust-lang/chalk/pull/272/files#diff-721709466568566f24fc2e8634c40dcbR140">https://github.com/rust-lang/chalk/pull/272/files#diff-721709466568566f24fc2e8634c40dcbR140</a></p>



<a name="180556566"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180556566" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180556566">(Nov 12 2019 at 20:16)</a>:</h4>
<p>Really we don't want auto-traits for these tests</p>



<a name="180556575"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180556575" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180556575">(Nov 12 2019 at 20:16)</a>:</h4>
<p>We just want a way to write "coinductive" traits</p>



<a name="180556582"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180556582" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180556582">(Nov 12 2019 at 20:16)</a>:</h4>
<p>maybe we should enable that</p>



<a name="180556598"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180556598" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180556598">(Nov 12 2019 at 20:16)</a>:</h4>
<p>auto-traits come with other baggage (i.e., implemented for all structs, etc)</p>



<a name="180556610"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180556610" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180556610">(Nov 12 2019 at 20:16)</a>:</h4>
<p>Hmm</p>



<a name="180556623"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180556623" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180556623">(Nov 12 2019 at 20:16)</a>:</h4>
<p>is there a separate way to mark a trait as coinductive only</p>



<a name="180556800"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180556800" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180556800">(Nov 12 2019 at 20:18)</a>:</h4>
<p>Right now, a goal is coinductive if 1) We ask if an auto trait is implemented or 2) It's a well-formed goal</p>



<a name="180558408"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180558408" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180558408">(Nov 12 2019 at 20:33)</a>:</h4>
<blockquote>
<p>is there a separate way to mark a trait as coinductive only</p>
</blockquote>
<p>no, but we could add one</p>



<a name="180558452"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180558452" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180558452">(Nov 12 2019 at 20:34)</a>:</h4>
<p>it would require a bit of threading</p>



<a name="180558461"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180558461" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180558461">(Nov 12 2019 at 20:34)</a>:</h4>
<p>we'd add a <code>#[coinductive]</code> attribute or something</p>



<a name="180558476"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180558476" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180558476">(Nov 12 2019 at 20:34)</a>:</h4>
<p>I've sometimes wondered if we can make <em>all</em> traits coinductive, but anyway</p>



<a name="180558514"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180558514" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180558514">(Nov 12 2019 at 20:34)</a>:</h4>
<p>Yeah, I was curious about that</p>



<a name="180558585"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180558585" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180558585">(Nov 12 2019 at 20:35)</a>:</h4>
<p>So, is it worth adding that? If so, in this PR or in a separate one? Otherwise, can't really test these two cases</p>



<a name="180558605"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180558605" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180558605">(Nov 12 2019 at 20:35)</a>:</h4>
<p>(at least, can't test that they go to no solution instead of floundering)</p>



<a name="180562681"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180562681" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180562681">(Nov 12 2019 at 21:15)</a>:</h4>
<p>It was easy enough to add and better tests the minimal "only coinductive" behavior we want to test so I added it</p>



<a name="180562697"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180562697" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180562697">(Nov 12 2019 at 21:15)</a>:</h4>
<p>And all the tests (for coinductiveness), so far, pass</p>



<a name="180562718"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180562718" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180562718">(Nov 12 2019 at 21:15)</a>:</h4>
<p>The <code>coinductive_semantics</code> test is actually and <code>auto_semantics</code> test</p>



<a name="180562814"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180562814" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180562814">(Nov 12 2019 at 21:16)</a>:</h4>
<p>(deleted)</p>



<a name="180563403"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180563403" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180563403">(Nov 12 2019 at 21:22)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> I have maybe a naive question</p>



<a name="180563404"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180563404" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180563404">(Nov 12 2019 at 21:22)</a>:</h4>
<p><code>C1(A, B) :- C1(B, A).</code></p>



<a name="180563445"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180563445" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180563445">(Nov 12 2019 at 21:22)</a>:</h4>
<p>I'm not exactly sure what haven't two variables here means</p>



<a name="180563485"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180563485" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180563485">(Nov 12 2019 at 21:23)</a>:</h4>
<p>So <code>C1(A) :- C2(A)</code> means <code>A: C1 if A: C2</code></p>



<a name="180566617"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180566617" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180566617">(Nov 12 2019 at 21:56)</a>:</h4>
<p><span class="user-mention" data-user-id="232957">@Jack Huey</span> you could model it as <code>(A, B): C1</code>, for example, or as <code>A: C1&lt;B&gt;</code></p>



<a name="180569136"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180569136" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180569136">(Nov 12 2019 at 22:28)</a>:</h4>
<p>Oh, that's good to know</p>



<a name="180643546"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180643546" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180643546">(Nov 13 2019 at 16:21)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> just wondering if you've gotten a chance to take a look at the coinductive PR?</p>



<a name="180692682"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180692682" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180692682">(Nov 14 2019 at 01:51)</a>:</h4>
<p>not today, will try to do that tomorrow <span class="user-mention" data-user-id="232957">@Jack Huey</span></p>



<a name="180692685"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180692685" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180692685">(Nov 14 2019 at 01:51)</a>:</h4>
<p>No problem</p>



<a name="180692731"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180692731" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180692731">(Nov 14 2019 at 01:52)</a>:</h4>
<p>I realized that I'm sort of in a dilemma with it</p>



<a name="180718012"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180718012" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180718012">(Nov 14 2019 at 10:34)</a>:</h4>
<p><span class="user-mention" data-user-id="232957">@Jack Huey</span> does this have to do you with your latest comment about floundering, or something else?</p>



<a name="180718171"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180718171" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180718171">(Nov 14 2019 at 10:36)</a>:</h4>
<p>(To start, I think we should rebase the "coinductive" attribute and land that, btw)</p>



<a name="180718358"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180718358" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180718358">(Nov 14 2019 at 10:38)</a>:</h4>
<p>OK, reading branch now. I'm going to try making a few edits and push to the branch, hope you don't mind. I just don't think i'll have much time today and this seems like fastest way to give feedback.</p>



<a name="180719434"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180719434" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180719434">(Nov 14 2019 at 10:53)</a>:</h4>
<p>OK, that may have been ambitious on my part. The main bit of feedback is that indeed the delayed subgoals have to be canonicalized together with the answer substitution. This implies that I think we have to add another associated type besides <code>CanonicalConstrainedSubst</code> -- I was trying to add one entitled <code>CanonicalAnswerSubst</code>, which would include the delayed subgoals. I am pondering where the delayed subgoals should be introduced to the ex-clause -- probably as part of <code>apply_answer_subst</code>, though I think that this code cannot really be expected to detect trivial-self-cycles... well, I guess why not? it already knows the goal.</p>



<a name="180719539"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180719539" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180719539">(Nov 14 2019 at 10:54)</a>:</h4>
<p>As a crazy nit-pick, I was tempted to suggest that <code>CompleteAnswer</code> should just be <code>Answer</code>, and that <code>Answer</code> should be <code>PartialAnswer</code> or something, but I'm not really sure if I like that. =)</p>



<a name="180719625"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180719625" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180719625">(Nov 14 2019 at 10:55)</a>:</h4>
<p>Ah yeah and the <code>ExClause</code> should not be storing <em>canonical</em> goals, just uncanonical ones</p>



<a name="180720592"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180720592" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180720592">(Nov 14 2019 at 11:08)</a>:</h4>
<p>well, I pushed a commit that starts going down that road, but it's not complete</p>



<a name="180737893"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180737893" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180737893">(Nov 14 2019 at 14:57)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> thanks for the feedback! I'll try to take the changes that you made and run with it</p>



<a name="180755996"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180755996" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180755996">(Nov 14 2019 at 17:58)</a>:</h4>
<p><a href="https://github.com/rust-lang/chalk/pull/285" target="_blank" title="https://github.com/rust-lang/chalk/pull/285">https://github.com/rust-lang/chalk/pull/285</a></p>



<a name="180756007"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180756007" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180756007">(Nov 14 2019 at 17:58)</a>:</h4>
<p>PR with just coinductive attribute + new tests</p>



<a name="180870137"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180870137" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180870137">(Nov 15 2019 at 20:47)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> you around?</p>



<a name="180870145"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180870145" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180870145">(Nov 15 2019 at 20:47)</a>:</h4>
<p>Question</p>



<a name="180870176"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180870176" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180870176">(Nov 15 2019 at 20:47)</a>:</h4>
<p>So, when we get non-trivial self-cycle subgoals in the answer for the root goal, those are <code>C::GoalInEnvironment</code></p>



<a name="180870252"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180870252" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180870252">(Nov 15 2019 at 20:48)</a>:</h4>
<p>If we want to reevaluate those, they need to be <code>C::UCanonicalGoalInEnvironment</code></p>



<a name="180870260"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180870260" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180870260">(Nov 15 2019 at 20:48)</a>:</h4>
<p>what's the correct way to convert that</p>



<a name="180906400"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180906400" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180906400">(Nov 16 2019 at 10:14)</a>:</h4>
<p>I'm not sure I understand the question yet</p>



<a name="180906413"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180906413" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180906413">(Nov 16 2019 at 10:15)</a>:</h4>
<p>Something seems wrong <span class="user-mention" data-user-id="232957">@Jack Huey</span> -- do you mean from <code>evaluate_root_goal</code> (or wherever we do the "answer refinement" stage)?</p>



<a name="180906474"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180906474" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180906474">(Nov 16 2019 at 10:17)</a>:</h4>
<p>I think the idea would be to make a strand within that same table, and I think it should only need goals</p>



<a name="180906479"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180906479" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180906479">(Nov 16 2019 at 10:17)</a>:</h4>
<p>Have you pushed to the PR?</p>



<a name="180926233"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180926233" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180926233">(Nov 16 2019 at 20:04)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> Yes I mean in <code>ensure_root_answer</code> (which I just renamed to <code>root_answer</code> and return the <code>CompleteAnswer</code>.</p>



<a name="180926238"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180926238" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180926238">(Nov 16 2019 at 20:05)</a>:</h4>
<p>Anyways, I ended up figuring it out</p>



<a name="180926242"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180926242" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180926242">(Nov 16 2019 at 20:05)</a>:</h4>
<p>and all the tests pass</p>



<a name="180926250"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180926250" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180926250">(Nov 16 2019 at 20:05)</a>:</h4>
<p>But, the way I approach is may not be (probably not) 100%</p>



<a name="180926297"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180926297" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180926297">(Nov 16 2019 at 20:06)</a>:</h4>
<p>Basically, in short, the "answer" for the root table may have non-trivial self-cycles as delayed subgoals</p>



<a name="180926300"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180926300" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180926300">(Nov 16 2019 at 20:06)</a>:</h4>
<p>But there are <code>C::GoalInEnvironment</code></p>



<a name="180926307"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180926307" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180926307">(Nov 16 2019 at 20:06)</a>:</h4>
<p>If we want to try to evaluate these, we need a <code>C::UCanonicalGoalInEnvironment</code></p>



<a name="180926371"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180926371" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180926371">(Nov 16 2019 at 20:08)</a>:</h4>
<p>I ended up just making a new function in <code>Context</code> which takes the <code>UCanonicalGoalInEnvironment</code> from the root goal and applies it's binders to the <code>GoalInEnvironment</code> for the delayed_subgoal</p>



<a name="180926381"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180926381" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180926381">(Nov 16 2019 at 20:09)</a>:</h4>
<p>Which I don't think is necessarily the correct way to do it. But it does work, at least for the current tests</p>



<a name="180926385"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180926385" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180926385">(Nov 16 2019 at 20:09)</a>:</h4>
<p>So,</p>



<a name="180926391"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180926391" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180926391">(Nov 16 2019 at 20:09)</a>:</h4>
<p>I'll clean up my changes locally and push to the PR for comments/review</p>



<a name="180926652"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/180926652" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#180926652">(Nov 16 2019 at 20:16)</a>:</h4>
<p>There's also other "assumptions" I've made currently that I don't think will always hold (but do for current tests), once I push these changes I'm gonna work on making some tests that break these</p>



<a name="181043089"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/181043089" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#181043089">(Nov 18 2019 at 18:39)</a>:</h4>
<p><span class="user-mention" data-user-id="232957">@Jack Huey</span> I took a peek at the commits so far, will do a more in-depth look later</p>



<a name="181043179"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/181043179" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#181043179">(Nov 18 2019 at 18:40)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> Any (general) comments?</p>



<a name="181043215"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/181043215" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#181043215">(Nov 18 2019 at 18:40)</a>:</h4>
<p>Not yet, it seemed "pretty close" -- the logic around what is a "trivial cycle" probably needs a bit of tweaking -- but yeah</p>



<a name="181043231"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/181043231" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#181043231">(Nov 18 2019 at 18:40)</a>:</h4>
<p>Ok</p>



<a name="181043442"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/181043442" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#181043442">(Nov 18 2019 at 18:43)</a>:</h4>
<p>The big thing right now I personally am <em>unsure</em> about are whether the way I'm handling the binders for delayed subgoals</p>



<a name="181043606"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/181043606" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#181043606">(Nov 18 2019 at 18:44)</a>:</h4>
<p>And I guess, in what cases might we have a substitution from a delayed subgoal and how do we incorporate that</p>



<a name="183092900"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183092900" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183092900">(Dec 10 2019 at 19:27)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> I'll have to update the branch to fix the new merge conflict from yesterday, but do you think you'll have time this week to review the coinduction branch?</p>



<a name="183107252"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183107252" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183107252">(Dec 10 2019 at 21:58)</a>:</h4>
<p><span class="user-mention" data-user-id="232957">@Jack Huey</span> yes</p>



<a name="183361160"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183361160" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183361160">(Dec 13 2019 at 14:02)</a>:</h4>
<p><span class="user-mention" data-user-id="232957">@Jack Huey</span> I've been looking it over. One thing that might be worth talking about -- perhaps as a standalone PR and a "pre-step" -- is having a mechanism to "invalidate" previous answers as having been superceded by newer ones. You remember how we were talking about what to do for <a href="https://github.com/rust-lang/chalk/issues/302" target="_blank" title="https://github.com/rust-lang/chalk/issues/302">https://github.com/rust-lang/chalk/issues/302</a>.</p>



<a name="183379512"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183379512" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183379512">(Dec 13 2019 at 17:12)</a>:</h4>
<p>So, unless I'm mistaken, for this it wouldn't actually do anything except maybe be a performance optimization?</p>



<a name="183380651"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183380651" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183380651">(Dec 13 2019 at 17:26)</a>:</h4>
<p>in some sense that's always true</p>



<a name="183380807"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183380807" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183380807">(Dec 13 2019 at 17:29)</a>:</h4>
<p>anyway, let me poke at this branch a bit</p>



<a name="183380817"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183380817" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183380817">(Dec 13 2019 at 17:29)</a>:</h4>
<p>Also, I think the answer invalidation in that issue is different than what would be used for conduction</p>



<a name="183380875"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183380875" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183380875">(Dec 13 2019 at 17:30)</a>:</h4>
<p>Maybe</p>



<a name="183380955"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183380955" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183380955">(Dec 13 2019 at 17:31)</a>:</h4>
<p>I don't think so</p>



<a name="183380959"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183380959" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183380959">(Dec 13 2019 at 17:31)</a>:</h4>
<p>basically just a way to say "there's a better answer later"</p>



<a name="183380994"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183380994" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183380994">(Dec 13 2019 at 17:32)</a>:</h4>
<p>or rather "this 'answer' turned out to be an error"</p>



<a name="183381017"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183381017" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183381017">(Dec 13 2019 at 17:32)</a>:</h4>
<p>but I don't think it's really a necessary pre-step, thinking more about it</p>



<a name="183381070"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183381070" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183381070">(Dec 13 2019 at 17:33)</a>:</h4>
<p>Tbh thinking about an "answer turning out to be an error" sounds scary</p>



<a name="183381195"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183381195" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183381195">(Dec 13 2019 at 17:34)</a>:</h4>
<p>heh</p>



<a name="183381205"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183381205" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183381205">(Dec 13 2019 at 17:34)</a>:</h4>
<p>I'm also not sure if the technical overhead is really worth whatever performance difference</p>



<a name="183381212"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183381212" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183381212">(Dec 13 2019 at 17:34)</a>:</h4>
<p>it's not so scary as it sounds</p>



<a name="183381232"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183381232" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183381232">(Dec 13 2019 at 17:35)</a>:</h4>
<p>like, if an answer includes delayed subgoals, then it's clear that an "answer" can lead to an error</p>



<a name="183381238"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183381238" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183381238">(Dec 13 2019 at 17:35)</a>:</h4>
<p>(i.e., processing those subgoals can fail)</p>



<a name="183381248"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183381248" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183381248">(Dec 13 2019 at 17:35)</a>:</h4>
<p>anyway, we can revisit after, I agree it's not a necessary step</p>



<a name="183382474"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183382474" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183382474">(Dec 13 2019 at 17:51)</a>:</h4>
<p><span class="user-mention" data-user-id="232957">@Jack Huey</span> do you happen to have that hackmd handy where we worked through the algorithm? I think I may see an opportunity for simplification here actually..</p>



<a name="183382498"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183382498" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183382498">(Dec 13 2019 at 17:51)</a>:</h4>
<p>I guess it was probably <a href="https://hackmd.io/OJRi5OM6Twunw8ZmuLxfRA" target="_blank" title="https://hackmd.io/OJRi5OM6Twunw8ZmuLxfRA">this one</a></p>



<a name="183382737"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183382737" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183382737">(Dec 13 2019 at 17:54)</a>:</h4>
<p>Yep that's it</p>



<a name="183382900"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183382900" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183382900">(Dec 13 2019 at 17:56)</a>:</h4>
<p>And indeed it points out to me why the simplification doesn't work</p>



<a name="183382908"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183382908" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183382908">(Dec 13 2019 at 17:56)</a>:</h4>
<p>Though I think there's still a simpler way to express things than the way I explained it in the doc</p>



<a name="183382968"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183382968" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183382968">(Dec 13 2019 at 17:57)</a>:</h4>
<p>In what way?</p>



<a name="183383020"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183383020" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183383020">(Dec 13 2019 at 17:58)</a>:</h4>
<p>Did i do something wrong</p>



<a name="183383096"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183383096" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183383096">(Dec 13 2019 at 17:59)</a>:</h4>
<p>let me try to "prove out" this real quick</p>



<a name="183383106"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183383106" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183383106">(Dec 13 2019 at 18:00)</a>:</h4>
<p>before I respond</p>



<a name="183383243"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183383243" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183383243">(Dec 13 2019 at 18:01)</a>:</h4>
<p>Sure</p>



<a name="183384826"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183384826" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183384826">(Dec 13 2019 at 18:21)</a>:</h4>
<p>Ok <span class="user-mention" data-user-id="232957">@Jack Huey</span> I pushed some commits to your branch</p>



<a name="183384835"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183384835" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183384835">(Dec 13 2019 at 18:21)</a>:</h4>
<p>the key idea is this:</p>



<a name="183384839"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183384839" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183384839">(Dec 13 2019 at 18:21)</a>:</h4>
<p>when -- in the root table --</p>



<a name="183384851"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183384851" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183384851">(Dec 13 2019 at 18:21)</a>:</h4>
<p>we publish an answer <code>A :- B |</code> with delayed subgoals <code>B</code></p>



<a name="183384856"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183384856" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183384856">(Dec 13 2019 at 18:21)</a>:</h4>
<p>we immediately create a new strand in that table <code>A :- B</code></p>



<a name="183384922"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183384922" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183384922">(Dec 13 2019 at 18:22)</a>:</h4>
<p>(the logic for doing that is perhaps mildly inefficient right now in its treatment of canonicalization)</p>



<a name="183384986"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183384986" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183384986">(Dec 13 2019 at 18:23)</a>:</h4>
<p>we can still consider the original answer valid; I marked it as <em>ambiguous</em> for now but I think that's not quite right, as my comment explains</p>



<a name="183384995"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183384995" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183384995">(Dec 13 2019 at 18:23)</a>:</h4>
<p>I haven't of course tried to test this :)</p>



<a name="183385312"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385312" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385312">(Dec 13 2019 at 18:26)</a>:</h4>
<p>That's an interesting approach</p>



<a name="183385343"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385343" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385343">(Dec 13 2019 at 18:27)</a>:</h4>
<p>And that could mean that replacing a previous answer is needed?</p>



<a name="183385392"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385392" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385392">(Dec 13 2019 at 18:27)</a>:</h4>
<p>well so</p>



<a name="183385441"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385441" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385441">(Dec 13 2019 at 18:28)</a>:</h4>
<p>actually I think we should just consider the previous answer -- when it propagates <em>out</em> from the table -- as an error</p>



<a name="183385450"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385450" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385450">(Dec 13 2019 at 18:28)</a>:</h4>
<p>because this follow-up strand will publish another one that is better</p>



<a name="183385489"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385489" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385489">(Dec 13 2019 at 18:28)</a>:</h4>
<p>but that was not really what I originally had in mind, at least not exactly</p>



<a name="183385496"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385496" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385496">(Dec 13 2019 at 18:28)</a>:</h4>
<p>I feel like the aggregator won't handle this correctly?</p>



<a name="183385513"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385513" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385513">(Dec 13 2019 at 18:29)</a>:</h4>
<p>ah, yeah, I think that's corect, I had planned to remove that logic</p>



<a name="183385527"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385527" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385527">(Dec 13 2019 at 18:29)</a>:</h4>
<p>I mean I think it's wrong for it to panic anyway</p>



<a name="183385540"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385540" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385540">(Dec 13 2019 at 18:29)</a>:</h4>
<p>well I know that's wrong</p>



<a name="183385550"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385550" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385550">(Dec 13 2019 at 18:29)</a>:</h4>
<p>but then the question is what to do instead :)</p>



<a name="183385552"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385552" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385552">(Dec 13 2019 at 18:29)</a>:</h4>
<p>Well that too. But also</p>



<a name="183385571"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385571" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385571">(Dec 13 2019 at 18:29)</a>:</h4>
<p>er, sorry, you meant the <em>answer</em> aggregator</p>



<a name="183385579"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385579" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385579">(Dec 13 2019 at 18:29)</a>:</h4>
<p>If the first answer is ambiguous</p>



<a name="183385595"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385595" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385595">(Dec 13 2019 at 18:30)</a>:</h4>
<p>yeah this is why ambiguous is not correct</p>



<a name="183385644"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385644" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385644">(Dec 13 2019 at 18:30)</a>:</h4>
<p>although</p>



<a name="183385650"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385650" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385650">(Dec 13 2019 at 18:30)</a>:</h4>
<p>Then we can no longer get a unique answer</p>



<a name="183385659"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385659" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385659">(Dec 13 2019 at 18:30)</a>:</h4>
<p>that's not true</p>



<a name="183385679"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385679" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385679">(Dec 13 2019 at 18:30)</a>:</h4>
<p>I'm not sure what the aggregator will do <em>but</em></p>



<a name="183385693"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385693" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385693">(Dec 13 2019 at 18:30)</a>:</h4>
<p>if you have two answers with the same substitution</p>



<a name="183385700"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385700" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385700">(Dec 13 2019 at 18:30)</a>:</h4>
<p>and one is ambiguous and the other not</p>



<a name="183385704"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385704" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385704">(Dec 13 2019 at 18:30)</a>:</h4>
<p>you can ignore the ambiguous one</p>



<a name="183385713"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385713" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385713">(Dec 13 2019 at 18:30)</a>:</h4>
<p>I was running into this with the associated types branch</p>



<a name="183385714"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385714" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385714">(Dec 13 2019 at 18:30)</a>:</h4>
<p>but likely the aggregator is not smart enough</p>



<a name="183385726"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385726" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385726">(Dec 13 2019 at 18:31)</a>:</h4>
<p>The aggregator assumes the answers can't unify</p>



<a name="183385736"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385736" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385736">(Dec 13 2019 at 18:31)</a>:</h4>
<p>and in any case the other consideration is when the refinement strand just outright fails</p>



<a name="183385746"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385746" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385746">(Dec 13 2019 at 18:31)</a>:</h4>
<p>in which case the first answer isn't <em>ambiguous</em>, it's just false</p>



<a name="183385749"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385749" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385749">(Dec 13 2019 at 18:31)</a>:</h4>
<p>So it makes the most generic form it can</p>



<a name="183385758"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385758" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385758">(Dec 13 2019 at 18:31)</a>:</h4>
<p>well it assumes that if they are different, yes</p>



<a name="183385765"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385765" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385765">(Dec 13 2019 at 18:31)</a>:</h4>
<p>anyway it's pretty dumb</p>



<a name="183385774"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385774" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385774">(Dec 13 2019 at 18:31)</a>:</h4>
<p>but I think really it shouldn't even be seeing the first answer</p>



<a name="183385777"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385777" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385777">(Dec 13 2019 at 18:31)</a>:</h4>
<p>I don't think there's any info to be gained from it</p>



<a name="183385781"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385781" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385781">(Dec 13 2019 at 18:32)</a>:</h4>
<p>(at least in this case)</p>



<a name="183385837"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385837" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385837">(Dec 13 2019 at 18:32)</a>:</h4>
<p>Right, which is why I did the refinement before returning a root answer</p>



<a name="183385846"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385846" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385846">(Dec 13 2019 at 18:32)</a>:</h4>
<p>yeah but</p>



<a name="183385860"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385860" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385860">(Dec 13 2019 at 18:32)</a>:</h4>
<p>it's easier to</p>



<a name="183385863"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385863" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385863">(Dec 13 2019 at 18:32)</a>:</h4>
<p>just return a marker value</p>



<a name="183385869"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385869" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385869">(Dec 13 2019 at 18:32)</a>:</h4>
<p>that's like "ignore me, find the next answer"</p>



<a name="183385916"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385916" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385916">(Dec 13 2019 at 18:33)</a>:</h4>
<p>Actually, this is where I think maybe the non-recursive changes can help us</p>



<a name="183385927"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385927" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385927">(Dec 13 2019 at 18:33)</a>:</h4>
<p>(conceptually the aggregator could even just ignore answers that have delayed subgoals, but I think it's somehow cleaner to hide that detail from outside the table)</p>



<a name="183385934"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385934" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385934">(Dec 13 2019 at 18:33)</a>:</h4>
<p>I haven't thought a ton about it yet</p>



<a name="183385954"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385954" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385954">(Dec 13 2019 at 18:33)</a>:</h4>
<p>hmm I don't see what they have to do with it :)</p>



<a name="183385961"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183385961" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183385961">(Dec 13 2019 at 18:34)</a>:</h4>
<p>But I think it should be clean enough to refine before returning</p>



<a name="183386004"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183386004" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183386004">(Dec 13 2019 at 18:34)</a>:</h4>
<p>you cannot refine before returning</p>



<a name="183386021"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183386021" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183386021">(Dec 13 2019 at 18:34)</a>:</h4>
<p>well</p>



<a name="183386023"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183386023" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183386023">(Dec 13 2019 at 18:34)</a>:</h4>
<p>what I mean is</p>



<a name="183386037"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183386037" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183386037">(Dec 13 2019 at 18:34)</a>:</h4>
<p>unless you want to have two distinct sets of answer indices</p>



<a name="183386056"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183386056" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183386056">(Dec 13 2019 at 18:34)</a>:</h4>
<p>the first answer is real, and has to be in the table</p>



<a name="183386075"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183386075" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183386075">(Dec 13 2019 at 18:34)</a>:</h4>
<p>unless maybe you are thinking to overwrite it in place</p>



<a name="183386101"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183386101" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183386101">(Dec 13 2019 at 18:35)</a>:</h4>
<p>but I don't think it's actually that clean</p>



<a name="183386102"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183386102" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183386102">(Dec 13 2019 at 18:35)</a>:</h4>
<p>Hmm</p>



<a name="183386107"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183386107" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183386107">(Dec 13 2019 at 18:35)</a>:</h4>
<p>e.g., consider this</p>



<a name="183386116"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183386116" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183386116">(Dec 13 2019 at 18:35)</a>:</h4>
<p>the table maybe have other strands that haven't completed yet</p>



<a name="183386129"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183386129" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183386129">(Dec 13 2019 at 18:35)</a>:</h4>
<p>and so if we publish an answer X</p>



<a name="183386132"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183386132" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183386132">(Dec 13 2019 at 18:35)</a>:</h4>
<p>and then create a strand to refine X</p>



<a name="183386169"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183386169" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183386169">(Dec 13 2019 at 18:35)</a>:</h4>
<p>trying to do that could lead to (e.g.) running out of quantum or fuel</p>



<a name="183386211"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183386211" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183386211">(Dec 13 2019 at 18:36)</a>:</h4>
<p>it's just a lot of state to juggle</p>



<a name="183386218"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183386218" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183386218">(Dec 13 2019 at 18:36)</a>:</h4>
<p>but in this approach, there really is no state</p>



<a name="183386229"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183386229" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183386229">(Dec 13 2019 at 18:36)</a>:</h4>
<p>we just say "you're looking for answer N? look for N+1"</p>



<a name="183386232"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183386232" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183386232">(Dec 13 2019 at 18:36)</a>:</h4>
<p>which we already have to do</p>



<a name="183386315"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183386315" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183386315">(Dec 13 2019 at 18:37)</a>:</h4>
<p>one thing I haven't quite decided yet: could it be that the refinement strand winds up with a different substitution -- or even multiple answers? I guess I have to think about that. Seems...plausible.</p>



<a name="183386360"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183386360" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183386360">(Dec 13 2019 at 18:37)</a>:</h4>
<p>I'll look over your changes</p>



<a name="183386369"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183386369" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183386369">(Dec 13 2019 at 18:37)</a>:</h4>
<p>But to answer that question</p>



<a name="183386433"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183386433" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183386433">(Dec 13 2019 at 18:38)</a>:</h4>
<p>For all current tests...no. I was ignoring that and everything "worked"</p>



<a name="183386446"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183386446" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183386446">(Dec 13 2019 at 18:38)</a>:</h4>
<p>I realize I already overlooked one bit of complexity in the "delayed trivial self cycle" walkthrough I did, in that indeed if we publish a new answer (a "refinement answer"), then our refinement strand will try to build on that too -- though it will lead to a duplicate answer, which I guess is ok</p>



<a name="183386459"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183386459" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183386459">(Dec 13 2019 at 18:38)</a>:</h4>
<p>But I don't know the answer for "all" cases</p>



<a name="183386653"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183386653" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183386653">(Dec 13 2019 at 18:40)</a>:</h4>
<p>Maybe I'll try to make a test</p>



<a name="183386670"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183386670" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183386670">(Dec 13 2019 at 18:40)</a>:</h4>
<p>in any case, the logic to create a refinement strand is "roughly" what we want</p>



<a name="183386672"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183386672" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183386672">(Dec 13 2019 at 18:40)</a>:</h4>
<p>(I think:)</p>



<a name="183386902"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183386902" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183386902">(Dec 13 2019 at 18:43)</a>:</h4>
<p>I'll take a look at trying to fix the tests</p>



<a name="183518553"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183518553" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183518553">(Dec 16 2019 at 04:20)</a>:</h4>
<p>Ok <span class="user-mention" data-user-id="116009">@nikomatsakis</span>, I took your changes and worked off of them. So, I don't think making an answer having delayed subgoals be "ambiguous" is the right idea (because the solver doesn't know if it should "consider that"). Instead, I made a new fail "InvalidAnswer". The other issue is now matching the delayed subgoal to the table goal (so it doesn't get added to the ex clause). So, I was checking this in <code>apply_answer_subst</code>, but with the changes you made, the bound variables (I think I got the right name?) in the delayed subgoals get unique inference variables compared to the table goal, so can't check equality. As it is, really they need to be checked after the answer subst is canonicalized (which is now in <code>pursue_answer</code>). For now, to make sure it works, I instead just filter the delayed subgoals  in <code>create_refinement_strand</code>, but this is a bit late, because the delayed subgoals are already in the <code>ExClause</code>.</p>



<a name="183518557"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183518557" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183518557">(Dec 16 2019 at 04:20)</a>:</h4>
<p>Oops that's a big blob of text</p>



<a name="183559031"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183559031" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183559031">(Dec 16 2019 at 15:26)</a>:</h4>
<p><span class="user-mention" data-user-id="232957">@Jack Huey</span> "invalid answer" sounds like exactly what I had in mind -- not sure about the rest yet, have to look maybe at the commit, did you push?</p>



<a name="183559160"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183559160" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183559160">(Dec 16 2019 at 15:27)</a>:</h4>
<p>Yes it's pushed</p>



<a name="183584913"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183584913" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183584913">(Dec 16 2019 at 20:02)</a>:</h4>
<p>OK, <span class="user-mention" data-user-id="232957">@Jack Huey</span>, I have to run to something else, but I'll try to look at this later on -- did you have specific questions?</p>



<a name="183584926"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183584926" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183584926">(Dec 16 2019 at 20:02)</a>:</h4>
<p>Nothing specific</p>



<a name="183584973"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183584973" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183584973">(Dec 16 2019 at 20:02)</a>:</h4>
<p>I need to spend some time and refactor the bit that I talked about (and has a FIXME), but it <em>works</em> now</p>



<a name="183584977"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/coinduction%20unsoundness/near/183584977" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/coinduction.20unsoundness.html#183584977">(Dec 16 2019 at 20:03)</a>:</h4>
<p>and tests pass</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>